(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(* (** ** Matrix Multiplication *) *)
Require Export List.
Require Export Matrix.Mat.Matrix_Module.
Require Import Matrix.MMat.MMat_def.
Require Import Matrix.MMat.Mlist_function.
Require Import Matrix.MMat.MMat_trans.
Import ListNotations.

Section Mul.
Variable A:Set.
Variable Zero:A.
Variable add:A->A->A.
Variable mul:A->A->A.
Variable m n p:nat.


(** *** ml_mul_dl *)
(** The multiplication of list and two-dimensional list. *)
Fixpoint ml_mul_dl (l:list (@Mat A m n)) (ma:list(list (@Mat A n p))) :=
  match ma with
  | nil => nil
  | a :: t 
    => product A Zero add mul m n p l a :: ml_mul_dl l t
  end.

(** *** mdl_mul_dl *)
(** The multiplication of two-dimensional lists. *)
Fixpoint mdl_mul_dl (left:list(list (@Mat A m n)))
  (right:list(list (@Mat A n p))) :=
  match left with
  | nil => nil
  | a :: t => ml_mul_dl a right 
  :: mdl_mul_dl t right
  end.

(** *** mat_mul_mat *)
(** The multiplication of matrices returns a two-dimensional list. *)
Definition mmat_mul_mat {m2 n2 p2:nat} (left:@Mat (@Mat A m n) m2 n2 ) 
  (right:@Mat (@Mat A n p) n2 p2):=
  let l1 := mat (@Mat A m n) m2 n2 left in
  let right' := trans (Mat A n p) (MO A Zero n p) right in
  let l2 := mat (@Mat A n p) p2 n2 right' in
    mdl_mul_dl l1 l2.

(** ** Properties of the Functions above   **)

(** *** length_l_mul_dl *)
(** The length of the list obtained by multiplying the list l and the
    two-dimensional list ma is equal to the height of ma. *)
Lemma length_ml_mul_dl : forall (l:list (@Mat A m n)) 
  (ma:list (list (@Mat A n p))), 
  length (ml_mul_dl l ma) = height ma.
Proof.
  intros l.
  induction ma.
  - simpl. auto.
  - simpl. rewrite IHma. auto.
Qed.
(*
(** *** width_dl_mul_dl_nilr *)
(** The width of the two-dimensional list obtained by the 
    multiplication of a two-dimensional list and nil is equal to 0. *)
Lemma width_dl_mul_dl_nilr: forall left , 
  width (dl_mul_dl left nil) 0.
Proof.
  induction left.
  - simpl. auto.
  - simpl. split. auto. auto.
Qed.
*)
(** *** height_dl_mul_dl *)
(** The height of the two-dimensional list obtained by the 
    multiplication of two-dimensional lists is equal to the height of
    the two-dimensional lists. *)
Lemma height_mdl_mul_dl : forall (left:list(list (@Mat A m n)))
  (right:list(list (@Mat A n p))),
  height (mdl_mul_dl left right) = height left.
Proof.
  induction left.
  - simpl. auto.
  - simpl. intros. rewrite IHleft. auto.
Qed.

(** *** width_dl_mul_dl *)
(** The width of the two-dimensional list obtained by the 
    multiplication of two-dimensional lists is equal to the width of
    the two-dimensional lists. *)
Lemma width_mdl_mul_dl : forall (n2:nat) (left:list(list (@Mat A m n)))
  (right:list(list (@Mat A n p))),
  height right = n2  -> width (mdl_mul_dl left right) n2.
Proof.
  induction n2.
  induction left.
  induction right.
  - simpl. auto.
  - simpl. intros. inversion H.
  - simpl. intros. split. rewrite length_ml_mul_dl. auto. apply IHleft. auto. 
  - induction left. induction right.
    + simpl. auto.
    + simpl. auto.
    + induction right.
      { simpl. intros. split. auto. inversion H. }
      { simpl. intros. split. rewrite length_ml_mul_dl. 
      auto. apply IHleft. auto. }
Qed.

(** *** height_mat_mul_mat *)
(** The height of the two-dimensional list obtained by the 
    multiplication of matrices is equal to the height of the matrices. *)
Lemma height_mmat_mul_mat : forall {m2 n2 p2:nat} (left:@Mat (@Mat A m n) m2 n2)
  (right :@Mat (@Mat A n p) n2 p2),
  height (mmat_mul_mat left right) = m2.
Proof.
  intros.
  unfold mmat_mul_mat.
  rewrite height_mdl_mul_dl.
  apply (mat_height (@Mat A m n) m2 n2 left).
Qed.

(** *** width_mat_mul_mat *)
(** The width of the two-dimensional list obtained by the 
    multiplication of matrices is equal to the width of the matrices. *)
Lemma width_mmat_mul_mat : forall {m2 n2 p2:nat} (left:@Mat (@Mat A m n) m2 n2)
  (right:@Mat (@Mat A n p) n2 p2),
  width (mmat_mul_mat left right) p2.
Proof.
  intros.
  unfold mmat_mul_mat.
  apply width_mdl_mul_dl. 
  apply (mat_height (@Mat A n p) p2 n2 (trans (Mat A n p) (MO A Zero n p) right)).
Qed.

(** ** matrix_mul *)
(** Matrix multiplication function : A × B. *)
Definition mmatrix_mul {m2 n2 p2:nat}
  (left :@Mat (@Mat A m n) m2 n2)(right:@Mat (@Mat A n p) n2 p2):=
  let ll := mmat_mul_mat left right in
  mkMat (@Mat A m p) m2 p2 ll (height_mmat_mul_mat left right)
                 (width_mmat_mul_mat left right).
End Mul.

Section Mul_validation .
Variable A:Set.
Variable Zero:A.
Variable add:A->A->A.
Variable mul:A->A->A.
Variable m n p:nat.

(*
Variable ma mb :@Mat A m n.
Variable mc md :@Mat A n p.
Definition mm1 :=mkMat_1_2 ma mb.
Definition mm1' := mkMat_2_1 mc md.
Definition mm2 := mkMat_1_1
  (Madd (Mmul ma mc)
  (Mmul mb md)).

Definition mmatrix_mul' := mmatrix_mul A Zero add mul .
Arguments mmatrix_mul'{m}{n}{p}{m2}{n2}{p2}.

Lemma mmatrix_mul_eq:
  (forall a, add a Zero = a) ->
  mmatrix_mul' mm1 mm1' == mm2.
Proof.
  unfold mm1,mm1',mm2,mmatrix_mul',mmatrix_mul,mmat_mul_mat,MM_eq.
  simpl. unfold M_eq,Mlist_function.Madd',Mmul,Mlist_function.mZero.
  unfold Madd',Madd,Mf,Mmul',matrix_mul,mat_mul_mat.
  unfold matrix_mul,mat_mul_mat,trans,mat_each.
  simpl. unfold mat_each. simpl. unfold mat_each.
  simpl. split. split. f_equal. rewrite ?trans_same.
  rewrite dlist_add_zero_r. auto. apply H.
  rewrite height_dl_mul_dl. apply (mat_height A m n mb).
  apply width_dl_mul_dl. apply height_gettrans.
  auto. auto.
Qed. 

Definition mm3 :=mkMat_2_1 ma mb.
Definition mm3' := mkMat_1_2 mc md.
Definition mm4 := mkMat_2_2
  (Mmul' ma mc)(Mmul' ma md)
  (Mmul' mb mc)(Mmul' mb md).

Lemma mmatrix_mul_eq2:
  (forall a, add a Zero = a) ->
  mmatrix_mul mm3 mm3' == mm4.
Proof.
  unfold mm1,mm1',mm2,mmatrix_mul,mmat_mul_mat,MM_eq.
  simpl. unfold M_eq,Mlist_function.Madd',Mmul,Mlist_function.mZero.
  unfold Madd',Madd,Mf,Mmul',matrix_mul,mat_mul_mat.
  unfold matrix_mul,mat_mul_mat,trans,mat_each.
  simpl. unfold mat_each. simpl. unfold mat_each.
  simpl. split. split. rewrite ?trans_same.
  rewrite dlist_add_zero_r. auto. apply H.
  rewrite height_dl_mul_dl. apply (mat_height A m n ma).
  apply width_dl_mul_dl. apply height_gettrans. apply (mat_height A p n mc).
  apply (mat_height A p n mc). apply ( mat_width A p n mc).
  rewrite ?trans_same. rewrite dlist_add_zero_r. split. auto.
  auto. apply H. rewrite height_dl_mul_dl. apply (mat_height A m n ma).
  apply width_dl_mul_dl. apply (mat_height A p n md).
  apply (mat_height A p n md). apply (mat_width A p n md).
  split. rewrite ?trans_same. rewrite dlist_add_zero_r.
  split. auto. split. rewrite dlist_add_zero_r. auto.
  apply H. rewrite height_dl_mul_dl. apply (mat_height A m n mb).
  apply width_dl_mul_dl. apply (mat_height A p n md). auto.
  apply H. rewrite height_dl_mul_dl. apply (mat_height A m n mb).
  apply width_dl_mul_dl. apply (mat_height A p n mc).
  apply (mat_height A p n md). apply (mat_width A p n md).
  apply (mat_height A p n mc). apply (mat_width A p n mc).
  auto.
Qed. 
*)

Lemma mdl_mul_dl_nil : forall m n p h ma,
  height ma = h ->
  mdl_mul_dl A Zero add mul m n p
  ma nil = nil_list(Mat A m p) h.
Proof.
  induction h. induction ma. simpl. auto.
  intros. inversion H. induction ma. intros. inversion H.
  intros. simpl. f_equal. apply IHh. inversion H. auto.
Qed.

Lemma ml_mul_dl_nil_list_r: forall m n p h a,
  ml_mul_dl  A Zero add mul m n p
  a (nil_list (Mat A n p) h) =
  list_o (Mat A m p) (MO A Zero m p) h.
Proof.
  induction h. - induction a. simpl. auto.
  simpl. auto. - induction a. simpl. f_equal.
  apply IHh. simpl. f_equal. apply IHh.
Qed.

Lemma mdl_mul_dl_nil_list_r: forall m n p h w ma,
  height ma = h -> 
  mdl_mul_dl A Zero add mul m n p ma (nil_list (Mat A n p) w) 
  = dlist_o (Mat A m p) (MO A Zero m p) h w.
Proof.
  induction h. induction ma. simpl. auto.
  intros. inversion H.
  induction ma. intros. inversion H.
  intros. simpl. f_equal. apply ml_mul_dl_nil_list_r.
  apply IHh. inversion H. auto.
Qed.

Lemma product'_app: forall h1 h2 l1 l2 l3 l4,
  (forall a, add Zero a = a)->(forall a, add a Zero = a)->
  length l1 = h1 -> length l3 = h1 ->
  length l2 = h2 -> length l4 = h2 ->
  (forall a b c , add a (add b c) = add (add a b) c)->
  product' A Zero add mul (l1++l2) (l3++l4) =
  add (product' A Zero add mul l1 l3)
      (product' A Zero add mul l2 l4).
Proof.
  induction h1.
  - induction l1. induction l3. simpl. intros. rewrite H.
    auto. intros. inversion H2. intros. inversion H1.
  - induction h2.
    + induction l2. induction l4. simpl. rewrite ?app_nil_r.  
      intros. rewrite H0. auto. intros. inversion H4.
      intros. inversion H3.
    + induction l1. intros. inversion H1. induction l3.
      intros. inversion H2. induction l2. intros. inversion H3.
      induction l4. intros. inversion H4. intros. simpl.
      rewrite IHh1 with(h2:= S h2). rewrite H5.
      f_equal. auto. auto. auto. auto. auto. auto.
      auto.
Qed.

Lemma l_mul_dl_mlink: forall h w1 w2  l1 l2 dl1 dl2, 
  length l1 = w1 -> length l2 = w2 ->
  height dl1 =h -> height dl2 = h-> 
  width dl1 w1 -> width dl2 w2 ->
  (forall a, add Zero a = a)->(forall a, add a Zero = a)->
  (forall a b c , add a (add b c) = add (add a b) c)->
  l_mul_dl A Zero add mul (l1 ++ l2) (mlink A dl1 dl2) =
  list_each A add (l_mul_dl A Zero add mul l1 dl1)
  (l_mul_dl A Zero add mul l2 dl2).
Proof.
  induction h.
  - induction dl1. induction dl2. simpl. auto.
    intros. inversion H2. intros. inversion H1.
  - induction w1. 
    + induction l1. simpl. intros.
      rewrite l_mul_dl_nil with(m:=S h).
      rewrite list_add_zero_l. 
      apply width_dlist_0 with(m:=S h)in H3.
      rewrite H3. rewrite mlink_nil_list_l. auto. auto.
      auto. auto. rewrite length_l_mul_dl. auto. auto.
      intros. inversion H.
    + induction w2. 
      * induction l2. intros. rewrite ?app_nil_r.
        apply width_dlist_0 with(m:=S h)in H4.
        rewrite H4. rewrite mlink_nil_list_r.
        rewrite l_mul_dl_nil_list. 
        rewrite list_add_zero_r. auto. auto.
        rewrite length_l_mul_dl. auto. auto. auto.
        intros. inversion H0.
      * induction l1. intros. inversion H.
        induction l2. intros. inversion H0.
        induction dl1. intros. inversion H1.
        induction dl2. intros. inversion H2.
        intros. simpl. f_equal.
        induction a1,a2. intros. inversion H3.
        inversion H8. inversion H3. inversion H8.
        inversion H4. inversion H8. simpl. rewrite <- H7.
        f_equal. rewrite product'_app with(h1:=w1)(h2:=S w2).
        f_equal. auto. auto. inversion H. auto.
        inversion H3. inversion H8. auto. auto. apply H4.
        auto. rewrite cons_app. rewrite IHh with(w1:=S w1)(w2:=S w2).
        f_equal. auto. auto. inversion H1. auto. inversion H2. auto.  
        apply H3. apply H4. auto. auto. auto.
Qed.



Lemma dl_mul_dl_mlink: forall h1 h2 w1 w2 dl1 dl2 dl3 dl4, 
  height dl1 = h1 -> height dl2 = h1 ->
  height dl3 = h2 -> height dl4 = h2 ->
  width dl1 w1 -> width dl3 w1->
  width dl2 w2 -> width dl4 w2 ->
  (forall a, add Zero a = a)->(forall a, add a Zero = a)->
  (forall a b c , add a (add b c) = add (add a b) c)->
  dl_mul_dl A Zero add mul 
  (mlink A dl1 dl2) (mlink A dl3 dl4) =
  mat_each' A add (dl_mul_dl A Zero add mul dl1 dl3)
  (dl_mul_dl A Zero add mul dl2 dl4).
Proof.
  induction h1.
  - induction dl1. simpl. induction dl2. simpl. auto.
    intros. inversion H0. intros. inversion H.
  - induction h2. 
    + induction dl3. induction dl4.
      intros. simpl. rewrite ?dl_mul_dl_nil with(m:= S h1).
      rewrite mat_each'_nil_list. auto.
      auto. auto. apply height_mlink. auto. auto.
      intros. inversion H2. intros. inversion H1.
    + induction dl1. intros. inversion H. induction dl2.
      intros. inversion H0. induction dl3. intros.
      inversion H1. induction dl4. intros. inversion H2.
      intros. simpl. f_equal. f_equal.
      apply product'_app with(h1:=w1)(h2:=w2). auto.
      auto. apply H3. apply H4. apply H5. apply H6.
      auto. apply l_mul_dl_mlink with(h:=h2)(w1:=w1)(w2:=w2).
      apply H3. apply H5. inversion H1. auto. inversion H2.
      auto. apply H4. apply H6. auto. auto. auto. 
      assert((a1 ++ a2) :: mlink A dl3 dl4 =mlink A (a1::dl3) (a2::dl4)).
      { auto. }
      rewrite H10. rewrite IHh1 with(h2:= S h2)(w1:=w1)(w2:=w2).
      auto. inversion H. auto. inversion H1. auto.
      auto. auto. apply H3. auto. apply H5. auto. auto.
      auto. auto.
Qed.

Lemma ml_mul_dl_nil_l: forall m n p h dl,
  height dl = h ->
  ml_mul_dl A Zero add mul m n p nil dl = list_o (Mat A m p) (MO A Zero m p) h.
Proof.
  induction h. induction dl. simpl. auto.
  intros. inversion H. induction dl. intros. inversion H.
  intros. simpl. f_equal. apply IHh. inversion H. auto.
Qed.

Lemma mlink_app: forall h1 h2 w1 w2 a b c d,
  height a = h1 -> height b = h1 -> 
  height c = h2 -> height d = h2 ->
  width a w1 -> width b w2 ->
  width c w1 -> width d w2 ->
  mlink A a b ++ mlink A c d = mlink A (a++c) (b++d).
Proof.
  induction h1. 
  - induction a. induction b. simpl. auto.
    intros. inversion H0. intros. inversion H.
  - induction h2. 
    + induction c,d. intros. simpl.
      rewrite ? app_nil_r. auto. intros. inversion H2.
      intros. inversion H1. intros. inversion H1.
    + induction a. intros. inversion H.
      induction b. intros. inversion H0.
      induction c. intros. inversion H1.
      induction d. intros. inversion H2.
      intros. simpl. f_equal. 
      rewrite <-IHh1 with(h2:=S h2)(w1:=w1)(w2:=w2).
      f_equal. inversion H. auto. inversion H0. auto.
      auto. auto. apply H3. apply H4. apply H5. apply H6.
Qed.

Lemma mlink_dl_mul_dl: forall h1 w1 w2 w3 dl1 dl2 dl3 ,
  height dl1 = h1 -> height dl2 = w1 -> height dl3 = w1 ->
  width dl1 w1 -> width dl2 w2 -> width dl3 w3 ->
  (forall a b : A, mul a b = mul b a) ->
  mlink A (dl_mul_dl A Zero add mul dl1 (gettrans A Zero dl2 w2))
  (dl_mul_dl A Zero add mul dl1 (gettrans A Zero dl3 w3)) =
  dl_mul_dl A Zero add mul dl1 ((gettrans A Zero dl2 w2) ++
  (gettrans A Zero dl3 w3)).
Proof.
  induction h1.
  - intros. apply length_zero_iff_nil in H. rewrite H.
    simpl. auto.
  - induction w1. 
    + induction dl2. induction dl3. intros. rewrite ?gettrans_nil.
      rewrite <- nil_list_app. rewrite ?dl_mul_dl_nil_list_r with(m:=S h1).
      rewrite mlink_dlist_o. auto. auto. auto. auto. auto. auto. auto.
      intros. inversion H1. intros. inversion H0.
    + induction dl1. intros. inversion H. induction dl2.
      intros. inversion H0. induction dl3. intros. inversion H1.
      intros. simpl. f_equal. rewrite l_mul_dl_app_r with(w:=S w1).
      auto. apply H2. apply width_gettrans. apply H0.
      apply width_gettrans. apply H1. rewrite IHh1 with(w1:=S w1).
      auto. inversion H. auto. apply H0. apply H1. apply H2.
      apply H3. auto. auto.
Qed.

  

Lemma lM_to_M1_ml_mul_dl: forall m n p h w l dl1 ,
  length l = h-> height dl1 = h -> width dl1  w->
  (forall a1 b : A, mul a1 b = mul b a1 )->
  (forall a1 : A, add Zero a1 = a1) ->
  (forall a1 : A, add a1 Zero = a1) ->
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  lM_to_M1 (ml_mul_dl  A Zero add mul m n p l 
  (gettrans (Mat A n p) (MO A Zero n p) dl1 w))
  = dl_mul_dl A Zero add mul(lM_to_M1 l)
  (dlM_to_M1 (mgettrans A Zero n p dl1 w) ).
Proof.
  induction h. - induction l. induction dl1. 
  intros. simpl. rewrite ml_mul_dl_nil_l with(h:=w).
  rewrite lM_to_M1_list_o. rewrite mgettrans_nil.
  rewrite dlM_to_M1_nil_list. 
  rewrite dl_mul_dl_nil_list_l with(n:=w*p0). auto.
  apply height_nil_list. apply height_gettrans.
  intros. inversion H0. intros. inversion H.
  - induction w. simpl. + intros. rewrite dl_mul_dl_nil with(m:= m0). auto.
  apply height_lM_to_M1.
  + induction l. intros. inversion H.
  induction dl1. intros. inversion H0.
  intros. simpl. unfold mat_each. simpl.
  rewrite IHw. rewrite dlM_to_M1_mgettrans with(h:=S h).
  simpl. rewrite gettrans_app_mlink with(h1:= n0)(h2:= h*n0).
  rewrite dl_mul_dl_mlink with(h1:=m0)(h2:=w * p0)(w1:=n0)(w2:=h*n0).
  rewrite <- mat_each'_mlink with(Zero:=Zero)(m:=m0)(n:=p0)(p:=w*p0).
  rewrite mlink_app with(h1:=p0)(h2:=w * p0)(w1:=n0)(w2:=h*n0).
  rewrite dl_mul_dl_mlink with(h1:=m0)(h2:=(S w)*p0)(w1:=n0)(w2:=h*n0).
  f_equal. rewrite mat_mhead. rewrite <- tailcolumn_n_lM_to_M1.
  unfold mat_mul_mat. simpl.
  rewrite <- mlink_dl_mul_dl with(h1:=m0)(w1:=n0).
  f_equal. f_equal. f_equal. rewrite headcolumn_n_lM_to_M1.
  auto. apply (mat_height A m0 n0 a).
  apply height_headcolumn_n. apply height_lM_to_M1.
  apply height_tailcolumn_n. apply height_lM_to_M1.
  apply (mat_width A m0 n0 a). apply width_headcolumn_n.
  apply width_tailcolumn_n. assert(p0+w*p0 = S w * p0).
  { auto. } rewrite H6. apply width_lM_to_M1. apply H1.
  auto. 
  assert(lM_to_M1 (mheadcolumn A Zero n0 p0 dl1) ++
   gettrans A Zero (dlM_to_M1 (tailcolumn (Mat A n0 p0) dl1))
     (w * p0) = dlM_to_M1 (mgettrans A Zero n0 p0 dl1 (S w))).
  { simpl. f_equal. rewrite dlM_to_M1_mgettrans with(h:= h).
    auto. apply height_tailcolumn. inversion H0. auto.
    apply width_tailcolumn. apply H1. }
  rewrite H6. rewrite <-IHh. simpl. f_equal. rewrite IHh.
  f_equal. rewrite dlM_to_M1_mgettrans with(h:= h).
  auto. apply height_tailcolumn. inversion H0. auto.
  apply width_tailcolumn. apply H1. inversion H. auto.
  apply height_tailcolumn. inversion H0. auto.
  apply width_tailcolumn. apply H1. auto.
  inversion H. auto. inversion H. auto. auto. inversion H. auto.
  inversion H0. auto. apply H1. auto. auto. auto. auto.
  apply (mat_height A m0 n0 a). apply height_lM_to_M1.
  simpl. apply height_app. apply (mat_height A p0 n0 (mhead A Zero n0 p0 a0)).
  apply height_gettrans. simpl. apply height_app.
  apply height_lM_to_M1. apply height_gettrans.
  apply (mat_width A m0 n0). apply width_app.
  split. apply (mat_width A p0 n0 (mhead A Zero n0 p0 a0)).
  apply width_gettrans. apply height_lM_to_M1.
  apply width_lM_to_M1. inversion H. auto. apply width_app.
  split. apply width_lM_to_M1. apply length_mheadcolumn.
  inversion H0. auto. apply width_gettrans. apply height_dlM_to_M1.
  apply height_tailcolumn. inversion H0. auto. auto. auto. auto.
  apply (mat_height A p0 n0 (mhead A Zero n0 p0 a0)).
  apply height_lM_to_M1. apply height_gettrans. apply height_gettrans.
  apply (mat_width A p0 n0 (mhead A Zero n0 p0 a0)).
  apply width_lM_to_M1. apply length_mheadcolumn.  inversion H0.
  auto. apply width_gettrans. apply height_lM_to_M1.
  apply width_gettrans. apply height_dlM_to_M1.
  apply height_tailcolumn. inversion H0. auto. auto.
  apply height_mat_mul_mat. rewrite height_dl_mul_dl.   
  apply (mat_height A m0 n0 a). 
  apply (mat_height A m0 p0 (product A Zero add mul m0 n0 p0 l
        (headcolumn (Mat A n0 p0) (MO A Zero n0 p0) dl1))).
  rewrite height_dl_mul_dl. apply height_lM_to_M1.
  apply width_mat_mul_mat. apply width_dl_mul_dl.
  apply height_gettrans. 
  apply (mat_width A m0 p0 (product A Zero add mul m0 n0 p0 l
        (headcolumn (Mat A n0 p0) (MO A Zero n0 p0)dl1))).
  apply width_dl_mul_dl. apply height_gettrans.
  apply (mat_height A m0 n0 a). apply height_lM_to_M1.
  apply height_gettrans. apply height_gettrans. 
  apply (mat_width A m0 n0 a). apply width_gettrans.
  apply height_lM_to_M1. apply width_lM_to_M1. inversion H.
  auto. apply width_gettrans. apply height_dlM_to_M1.
  apply height_tailcolumn. inversion H0. auto. auto. auto.
  auto. apply height_lM_to_M1. apply height_dlM_to_M1.
  apply height_tailcolumn. inversion H0. auto.
  apply width_lM_to_M1. apply length_tl. apply H1.
  apply width_dlM_to_M1. apply width_tailcolumn. apply H1.
  simpl. f_equal. apply height_tailcolumn. inversion H0.
  auto. simpl. split. apply length_tl. apply H1.
  apply width_tailcolumn. apply H1. apply H. simpl.
  f_equal. apply height_tailcolumn. inversion H0.
  auto. simpl. split. apply length_tl. apply H1.
  apply width_tailcolumn. apply H1. auto. auto. auto.
  auto.
Qed.
  

Lemma dlM_to_M1_mdl_mul_dl: forall m n p m2 n2 p2  (ma1:list (list (Mat A m n)))
  (ma2:list (list (Mat A n p))),
  height ma1 = m2 -> width ma1 n2 -> height ma2 = n2 -> width ma2 p2->
  (forall a1 b : A, mul a1 b = mul b a1 )->
  (forall a1 : A, add Zero a1 = a1) ->
  (forall a1 : A, add a1 Zero = a1) ->
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  dlM_to_M1 (mdl_mul_dl A Zero add mul m n p
  ma1 (gettrans (Mat A n p) (MO A Zero n p) ma2 p2)) =
  dl_mul_dl A Zero add mul (dlM_to_M1 ma1)
  (gettrans A Zero (dlM_to_M1 ma2) (p2 * p)).
Proof.
  induction m2. - induction ma1. simpl. auto. intros. inversion H.
  - induction n2. + induction ma1. intros. 
    inversion H. induction ma2. intros. simpl.
    rewrite ?gettrans_nil.
    rewrite dl_mul_dl_nil_list with(h:=(S m2)*m0). 
    rewrite mdl_mul_dl_nil_list_r with(h:= m2).
    rewrite ml_mul_dl_nil_list_r.
    rewrite dlM_to_M1_dlist_o. 
    assert(S m2 * m0 = m0+ m2*m0). { auto. }
    rewrite H7. rewrite dlist_o_app. f_equal.
    rewrite lM_to_M1_list_o. auto.
    inversion H. auto. apply height_app.
    apply height_lM_to_M1. apply height_dlM_to_M1.
    inversion H. auto. intros. inversion H1.
    + induction ma1. intros. inversion H.
      induction ma2. intros. inversion H1.
      intros. simpl. rewrite dl_mul_dl_app_l with(h1:=m0)(h2:=m2*m0).
      f_equal. assert(lM_to_M1 a0 ++ dlM_to_M1 ma2 =dlM_to_M1(a0::ma2)).
      { auto. } rewrite H7. rewrite <- dlM_to_M1_mgettrans with(h:=S n2).
      apply lM_to_M1_ml_mul_dl with(h:= S n2).
      apply H0. apply H1. apply H2. auto. auto. auto. auto.
      auto. apply H2.
      apply IHm2 with(n2:=S n2).
      inversion H.  auto. apply H0. auto.  auto. auto.
      auto. auto. auto. apply height_lM_to_M1.
      apply height_dlM_to_M1. inversion H0. inversion H.
      auto.
Qed.
  

Variable m2 n2 p2:nat.
Variable me :Mat (Mat A m n) m2 n2.
Variable mf :Mat (Mat A n p) n2 p2.
(*
Lemma mat_mhead: forall m0 n0 (mm: list (Mat A m0 n0)),
  gettrans A Zero (headcolumn_n A Zero (lM_to_M1 mm) n0) n0 =
  mat A n0 m0 (mhead A Zero m0 n0 mm).
Proof.
  induction mm. simpl. f_equal.
  rewrite headcolumn_n_nil_list. auto.
  simpl. f_equal. rewrite headcolumn_n_mlink with(h:=m0).
  auto. apply (mat_height A m0 n0 a). apply height_lM_to_M1.
  apply (mat_width A m0 n0 a). 
Qed.

Lemma lM_to_M_mheadoclumn: forall h w m0 n0 (mm: list (list (Mat A m0 n0))),
  height mm = h -> width mm w ->
  lM_to_M1 (mheadcolumn A Zero m0 n0 mm) =
  gettrans A Zero (headcolumn_n A Zero (dlM_to_M1 mm) n0) n0.
Proof.
  induction h.
  induction mm.  simpl. rewrite gettrans_nil. auto.
  intros. inversion H.
  induction mm. intros. inversion H. intros. simpl.
  rewrite headcolumn_n_app with(h1:=m0)(h2:=h*m0).
  rewrite gettrans_app_mlink with(h1:=m0)(h2:=h*m0).
  f_equal. rewrite mat_mhead. auto.
  apply IHh with(w:=w). inversion H. auto. apply H0.
  apply height_headcolumn_n. 
  apply height_lM_to_M1. apply height_headcolumn_n.
  apply height_dlM_to_M1. inversion H. auto.
  apply width_headcolumn_n. apply width_headcolumn_n.
  apply height_lM_to_M1. apply height_dlM_to_M1. inversion H.
  auto.
Qed.

Lemma lM_to_M1_tail: forall m0 n0 (a:list(Mat A m0 n0)), 
  tailcolumn_n A (lM_to_M1 a) n0 =
  lM_to_M1 (tail (Mat A m0 n0) a).
Proof.
  induction a. simpl. rewrite tailcolumn_n_nil_list. auto.
  simpl. apply tailcolumn_n_mlink with(h:=m0).
  apply (mat_height A m0 n0 a). apply height_lM_to_M1.
  apply (mat_width A m0 n0 a).
Qed.

Lemma dlM_to_M1_tailcolumn:forall  m0 n0 (mm:list(list(Mat A m0 n0))),
  tailcolumn_n A (dlM_to_M1 mm) n0 =
  dlM_to_M1 (tailcolumn (Mat A m0 n0) mm).
Proof.
  induction mm. simpl. auto.
  simpl. rewrite tailcolumn_n_app. f_equal. 
  apply lM_to_M1_tail. apply IHmm.
Qed.

Lemma dlM_to_M1_mgettrans: forall h w (mm:list (list (Mat A n p))),
  height mm  = h -> width mm w->
  gettrans A Zero (dlM_to_M1 mm) (w*p)
  = dlM_to_M1 (mgettrans A Zero n p mm w).
Proof.
  induction h. - induction mm. intros. simpl.
  rewrite gettrans_nil. rewrite mgettrans_nil.
  rewrite dlM_to_M1_nil_list. auto. intros. inversion H.
  - induction w. simpl. auto.
    + induction mm. intros. inversion H.
      intros. simpl. rewrite gettrans_app. f_equal.
      rewrite headcolumn_n_app with(h1:=n)(h2:=h*n).
      rewrite gettrans_app_mlink with(h1:=n)(h2:=h*n).
      f_equal. apply mat_mhead. rewrite lM_to_M1_mheadcolumn with(h:=h).
      auto. inversion H. auto. apply height_headcolumn_n. 
      apply height_lM_to_M1. apply height_headcolumn_n.
      apply height_dlM_to_M1. inversion H. auto.
      apply width_headcolumn_n. apply width_headcolumn_n.
      apply height_lM_to_M1. apply height_dlM_to_M1. inversion H.
      auto. rewrite <-IHw. f_equal. simpl. rewrite tailcolumn_n_app.
      f_equal. apply lM_to_M1_tail. apply dlM_to_M1_tailcolumn.
      simpl. f_equal. apply height_tailcolumn. inversion H. auto.
      simpl. split. apply length_tail. apply H0. apply width_tailcolumn.
      apply H0. apply width_app. assert(p+w*p =(S w)*p). 
      { auto. } rewrite H1. split. apply width_lM_to_M1. apply H0.
      apply width_dlM_to_M1. apply H0. apply width_headcolumn_n.
      apply width_tailcolumn_n.  assert(p+w*p =(S w)*p). 
      { auto. } rewrite H1.  apply width_app. split. apply width_lM_to_M1.
      apply H0. apply width_dlM_to_M1. apply H0.
Qed.
*)


Lemma MMmul_eq_Mmul: 
  (forall a1 b : A, mul a1 b = mul b a1 )->
  (forall a1 : A, add Zero a1 = a1) ->
  (forall a1 : A, add a1 Zero = a1) ->
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  MM_to_M (mmatrix_mul A Zero add mul m n p me mf) 
  === matrix_mul A Zero add mul(MM_to_M me)(MM_to_M mf).
Proof.
  unfold MM_to_M,MM_to_M',mmatrix_mul,mmat_mul_mat,matrix_mul,mat_mul_mat,M_eq.
  simpl. induction me,mf. simpl. 
  apply dlM_to_M1_mdl_mul_dl with(m2:=m2)(n2:=n2).
  auto. auto. auto. auto.
Qed.

End Mul_validation.

Section MMmul_lemma.
Variable A:Set.
Variable Zero :A.
Variable f:A->A->A.
Variable add mul:A->A->A.

Lemma mmatrix_mul_distr_l : forall{m n p m2 n2 p2:nat} 
  (ma mb: Mat (Mat A m n) m2 n2) (mc:Mat (Mat A n p) n2 p2), 
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul (f a b)c = f (mul a c) (mul b c))->
  (forall a1 b : A, mul a1 b = mul b a1 )->
  (forall a1 : A, add Zero a1 = a1) ->
  (forall a1 : A, add a1 Zero = a1) ->
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  mmatrix_mul A Zero add mul m n p 
    ( matrix_each (Mat A m n) (matrix_each A f) ma mb) mc ==
  matrix_each (Mat A m p) (matrix_each A f) 
  (mmatrix_mul A Zero add mul m n p ma mc)
  (mmatrix_mul A Zero add mul m n p mb mc).
Proof.
  intros. rewrite MM_to_M_M_eq. rewrite MMmul_eq_Mmul.
  rewrite ?MM_to_M_matrix_each. rewrite ?MMmul_eq_Mmul.
  apply matrix_mul_distr_l. auto. auto. auto. auto. auto.
  auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
  auto. auto.
Qed.

Lemma mmatrix_mul_distr_r: forall{m n p m2 n2 p2:nat} 
  (ma: Mat (Mat A m n) m2 n2) (mb mc:Mat (Mat A n p) n2 p2),
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c : A, mul a (f b c) = f (mul a b) (mul a c)) ->
  (forall a1 b : A, mul a1 b = mul b a1 )->
  (forall a1 : A, add Zero a1 = a1) ->
  (forall a1 : A, add a1 Zero = a1) ->
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  mmatrix_mul A Zero add mul m n p ma
    ( matrix_each (Mat A n p) (matrix_each A f) mb mc) ==
  matrix_each (Mat A m p) (matrix_each A f) 
  (mmatrix_mul A Zero add mul m n p ma mb)
  (mmatrix_mul A Zero add mul m n p ma mc).
Proof.
  intros. rewrite MM_to_M_M_eq. rewrite MMmul_eq_Mmul.
  rewrite ?MM_to_M_matrix_each. rewrite ?MMmul_eq_Mmul.
  apply matrix_mul_distr_r. auto. auto. auto. auto. auto.
  auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
  auto. auto.
Qed.

Lemma mmatrix_mul_zero_l: forall {m n p m2 n2 p2:nat} 
  (ma:Mat (Mat A n p) n2 p2),
  (forall a,mul Zero a = Zero) ->
  (forall a,add Zero a = a) ->
  (forall a1 : A, add a1 Zero = a1)->
  (forall a1 b : A, mul a1 b = mul b a1) -> 
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  mmatrix_mul A Zero add mul m n p 
  (MO (Mat A m n) (MO A Zero m n) m2 n2) ma 
  ==  (MO (Mat A m p) (MO A Zero m p) m2 p2).
Proof. 
  intros. rewrite MM_to_M_M_eq. rewrite MMmul_eq_Mmul.
  rewrite ?MM_to_M_MO. apply matrix_mul_zero_l.
  auto. auto. auto. auto. auto. auto.
Qed.

Lemma mmatrix_mul_zero_r: forall {m n p m2 n2 p2:nat} 
  (ma:Mat (Mat A m n) m2 n2),
  (forall a,mul a Zero = Zero) ->
  (forall a,add Zero a = a) ->
  (forall a1 : A, add a1 Zero = a1)->
  (forall a1 b : A, mul a1 b = mul b a1) -> 
  (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
  mmatrix_mul A Zero add mul m n p ma
  (MO (Mat A n p) (MO A Zero n p) n2 p2)  
  ==  (MO (Mat A m p) (MO A Zero m p) m2 p2).
Proof.
  intros. rewrite MM_to_M_M_eq. rewrite MMmul_eq_Mmul.
  rewrite ?MM_to_M_MO. apply matrix_mul_zero_r.
  auto. auto. auto. auto. auto. auto. auto.
Qed.

Lemma mmatrix_mul_assoc: forall  {m n p k m2 n2 p2 k2:nat} 
  (ma: Mat (Mat A m n) m2 n2)
  (mb: Mat (Mat A n p) n2 p2)
  (mc: Mat (Mat A p k) p2 k2),
  (forall a,add Zero a = a) ->
  (forall a, add a Zero = a)->
  (forall a b c, add a (add b c) = add (add a b) c)->
  (forall a, mul a Zero = Zero) ->
  (forall a, mul Zero a = Zero) ->
  (forall a b, mul a b = mul b a) ->
  (forall a b c, mul (mul a b) c = mul a (mul b c)) ->
  (forall a b c, mul a (add b c) = add (mul a b) (mul a c))->
  (forall a b c, mul (add b c) a = add (mul b a) (mul c a))->
  (forall a b c d : A,
  add (add a b) (add c d) = add (add a c) (add b d))->
  mmatrix_mul A Zero add mul m p k
  (mmatrix_mul A Zero add mul m n p ma mb) mc ==
  mmatrix_mul A Zero add mul m n k ma 
  (mmatrix_mul A Zero add mul n p k mb mc).
Proof.
  intros. rewrite MM_to_M_M_eq. rewrite ?MMmul_eq_Mmul.
  apply matrix_mul_assoc. auto. auto. auto. auto. auto.
  auto. auto. auto. auto. auto. auto. auto. auto. auto.
  auto. auto. auto. auto. auto. auto. auto. auto. auto.
  auto. auto.
Qed.

Lemma mmtrans_mul: forall  {m n p m2 n2 p2:nat}
  (ma: Mat (Mat A m n) m2 n2)
  (mb: Mat (Mat A n p) n2 p2),
  (forall a : A, add Zero a = a)->
  (forall a : A, add a Zero = a)->  
  (forall a b : A, mul a b = mul b a)->
  (forall a b c : A, add a (add b c) = add (add a b) c) ->
  mmtrans A Zero m p
  (mmatrix_mul A Zero add mul m n p ma mb) ==
  mmatrix_mul A Zero add mul p n m 
  (mmtrans A Zero n p mb)(mmtrans A Zero m n ma).
Proof.
  intros.
  rewrite MM_to_M_M_eq. rewrite ?MMmul_eq_Mmul.
  rewrite ?MMtrans_eq_Mtrans. rewrite ?MMmul_eq_Mmul.
  apply teq_mul. auto. auto. auto. auto. auto. auto.
  auto. auto. auto. auto.
Qed.

End MMmul_lemma.
